(DEFPROP ATTEMPT 
 (LAMBDA(Z S C)
  (PROG (NEWNAME SUPPORT
 		 EDITSTRAT
 		 LCL
 		 LVL
 		 CNT
 		 LSTCLS
 		 LLST
 		 Z1
 		 MERGE
 		 ORDER
 		 DEBUG
 		 DEPTH
 		 LENGTH
 		 ANCESTRY
 		 STRATEGY
 		 STRAT
 		 PMODEL
 		 NMODEL
 		 PFLG
 		 PDEPTH
 		 DLIST
 		 XYZ
 		 XYZ1
 		 COND
 		 UNAXP
 		 UNAXN
 		 SAT
 		 EE
 		 EE1
 		 CLAUSES
 		 SUBCLAUSES
 		 COUNT)
	(SETQ TBL (SET1 (APPEND PREFN INFN)))
	(SET3 Z)
	(SETQ Z (MINIMIZE Z))
	(SETQ NEWNAME (INITIAL Z))
	(SETQ CLAUSES Z)
	(UPDATESTATE (COND ((NULL S) (SETQ STRAT (SETQUERY Z))) (T (SETQ STRAT S))))
	(SETQ COND C)
	(SETQ LVL 1)
	(SETQ COUNT 0)
	(SETQ Z (UNITPN Z))
	(SETQ UNAXP (CAR Z))
	(SETQ UNAXN (CDR Z))
	(COND ((NOT PFLG) (SETQ UNAXP (CONS (SET2 (LIST (LIST 1 NIL) (LIST EQUAL 0 0))) UNAXP))
			  (SETQ SUBCLAUSES (CONS (CAR UNAXP) CLAUSES)))
	      (T (SETQ SUBCLAUSES CLAUSES)))
	(SETQ LCL (LAST CLAUSES))
	(SETQ LSTCLS LCL)
	(SETQ XYZ (SETQ EE CLAUSES))
	(SETQ EE1 (LAST CLAUSES))
   BB   (SETQ LLST (CONS (CAR XYZ) LLST))
	(SETQ XYZ (CDR XYZ))
	(COND (XYZ (GO BB)))
	(SETQ Z1 (ERRSET (TRYIT)))
	(COND ((OR (EQ Z1 (QUOTE NOPROOF)) (NULL Z1)) (RETURN (SETQUERY1 CLAUSES STRAT)))
	      ((EQ (CAR Z1) (QUOTE QED)) (SETQ Z
					       (EVAL
						(LIST (QUOTE OUTC)
						      (LIST (QUOTE OUTPUT)
							    (QUOTE PRF)
							    (QUOTE DSK:)
							    (CONS (READLIST
								   (CONS (QUOTE N)
									 (CONS (SETQ PRNO (ADD1 PRNO))
 									       FILENAM)))
								  (QUOTE PRF)))
 						      NIL)))
					 (QUERY)
					 (PROOF LHP RHP)
					 (OUTC Z T)
					 (RETURN Z1))
	      (T (RETURN Z1))))) 
EXPR)